The sentential decision diagram (SDD) has been recently proposed as a new tractable representation of Boolean functions that generalizes the influential ordered binary decision diagram (OBDD). Empirically, compiling CNFs into SDDs has yielded significant improvements in both time and space over compiling them into OBDDs, using a bottom-up compilation approach. In this work, we present a top-down CNF to SDD compiler that is based on techniques from the SAT literature. We compare the presented compiler empirically to the state-of-the-art, bottom-up SDD compiler, showing orders-of-magnitude improvements in compilation time.

The sentential decision diagram (SDD) has been recently proposed as a new  tractable representation of Boolean functions that generalizes the influential  ordered binary decision diagram (OBDD).  Empirically, compiling CNFs into SDDs  has yielded significant improvements in both time and space over compiling  them into OBDDs, using a bottom-up compilation approach. In this work, we present a top-down CNF to SDD compiler that is based on techniques  from the SAT literature. We compare the presented compiler empirically to the state-of-the-art, bottom-up SDD compiler, showing orders-of-magnitude improvements in compilation time.